FDL - Nuprl Lemma : weak-antecedent-functions-compose

Nuprl Lemma : weak-antecedent-functions-compose

es:ES, P, Q, R:(E

), f:({e:E| P(e)}

{e:E| Q(e)} ), g:({e:E| Q(e)}

{e:E| R(e)} ).
(Q

==f== P & R

==g== Q)

==g o f== P

Definitions E, f(a), {x:A| B(x)} , x:AB(x), e c e', x:A B(x), P & Q, x:A. B(x), Q ==f== P, P Q, Type, , ES, t T, f o g

Lemmas es-causle transitivity

Definitions	E, f(a), {x:A\| B(x)} , x:AB(x), e c e', x:A B(x), P & Q, x:A. B(x), Q ==f== P, P Q, Type, , ES, t T, f o g
Lemmas	es-causle transitivity